1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. $\forall$${\it bs}$:($T$ List). nth\_tl($\parallel$$v$$\parallel$;$v$ @ ${\it bs}$) $\sim$ ${\it bs}$
\\[0ex]$\vdash$  $\forall$${\it bs}$:($T$ List). nth\_tl($\parallel$$v$$\parallel$+1;[$u$ / ($v$ @ ${\it bs}$)]) $\sim$ ${\it bs}$